| Definitions |  x:A. B(x), State(ds), P   Q, t  T, Prop, Top,   x. t(x), P  Q, P Q, P & Q, Id, xL. P(x), DeclaredType(ds;x), if b t else f fi, true, false, x,y. t(x;y), Knd, A || B, Y, Rplus?(x1), Rplus-left(x1), Rplus-right(x1), Rnone?(x1), True, R-loc(R), Rds(R), Rda(R), p = q, R-base-domain(R), R-frame-compat(A;B), R-interface-compat(A;B), p  q, i=j, 1of(t), p  q, 2of(t), Reffect?(x1), Rframe?(x1), Rframe-x(x1), Reffect-x(x1), Reffect-knd(x1), Rframe-L(x1), Raframe?(x1), Raframe-k(x1), Raframe-L(x1), Rrframe?(x1), Rrframe-x(x1), Reffect-ds(x1), Rrframe-L(x1), Rsends?(x1), Rsframe?(x1), Rsframe-lnk(x1), Rsends-l(x1), Rsframe-tag(x1), Rsends-g(x1), Rsends-knd(x1), Rsframe-L(x1), Rbframe?(x1), Rbframe-k(x1), Rbframe-L(x1), Rsends-ds(x1), Rpre?(x1), Rpre-ds(x1), Rpre-a(x1), Rsends-dt(x1), Reffect-T(x1), Rsends-T(x1), SQType(T), {T}, A & B, P Q,  T, e@i. P(e), e' e.P(e'), e  e' , es-trans-state-from{i:l}(es;ks;g;z;e1;e2), event-info(ds;da), es-info(es;e), list_accum(x,a.f(x;a);y;l), let x,y,z = a in t(x;y;z), f(x)?z, state@i, Valtype(da;k), es-hist{i:l}(es;e1;e2), map(f;as), x(s), (x l),  , Unit,  x:A. B(x), x(s1,s2),  A, False, @i only events in L change x : T, WellFnd{i}(A;x,y.R(x;y)), (e <loc e'), @i events of kind k change x to f State(ds) (val:T), (state when e),  , x when e, s.x, R-state-var(i;ds;da;x;T;ks;tr) |
| Lemmas | l member wf, subtype rel dep function, fpf-cap wf, top wf, subtype rel self, fpf-cap-join-subtype, fpf-compatible-join-cap, id-deq wf, fpf-single wf, fpf-cap-single1, ma-valtype wf, decl-state wf, fpf-join wf, normal-da wf, normal-ds wf, Knd wf, assert wf, isrcv wf, Id wf, ldst wf, lnk wf, normal-type wf, fpf-compatible wf, fpf wf, R-effect-rule, fpf-join-cap-sq, fpf-trivial-subtype-top, fpf-cap-single, eqof eq btrue, fpf-dom wf, bool wf, eqtt to assert, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, normal-ds-join, normal-ds-single, normal-valtype, R-all-rule2, Reffect wf, effect-p wf, event system wf, decidable equal Kind, eq id wf, assert-eq-id, Id sq, band wf, eq knd wf, assert of band, and functionality wrt iff, assert-eq-knd, bor wf, squash wf, true wf, bnot thru band, assert of bor, or functionality wrt iff, not functionality wrt iff, fpf-compatible-self, fpf-compatible-singles, Kind-deq wf, IdLnk wf, R-frame-rule, R-and-rule, Rall wf, Rframe wf, frame-p wf, R-compat-symmetry, R-compat-Rall, fpf-compatible-join, fpf-compatible-symmetry, deq wf, fpf-empty-compatible-left, R-implies-rule, R-state-var wf, es-locl wf, es-after wf, es-le-loc, es-vartype wf, es-decls wf, es-loc wf, es-E wf, es-locl-wellfnd, es-loc-pred, es-locl-iff, es-le-iff, es-pred wf, es-pred-locl, es-after-pred, es-decls-iff, es-hist-last, es-isrcv wf, es-le-pred, list accum append, es-hist wf, subtype rel list, event-info wf, deq-member wf, es-kind wf, assert-deq-member, fpf-ap-equal, es-state-when wf, es-val wf, list accum wf, es-interval-eq2, subtype rel transitivity, subtype-fpf-cap-top, fpf-sub-join-left2, fpf-sub weakening, es-when wf |
Type, da:k:Knd fp
tr:(k:{k:Knd| (k 
T